the_w:World, e:E.
FairFifo
 isrcv(kind(e))
 (t:time(e).
 (match(lnk(kind(e));t;time(e))
 (& 0||rcvs(lnk(kind(e));time(e))||-||snds(lnk(kind(e));t)||
 (& & ||rcvs(lnk(kind(e));time(e))||-||snds(lnk(kind(e));t)||<||onlnk(lnk(kind(e))
 (& & ||rcvs(lnk(kind(e));time(e))||-||snds(lnk(kind(e));t)||<||onlnk;m(source(lnk(kind(e)));t))||
 (& & onlnk(lnk(kind(e));m(source(lnk(kind(e)));t))
 (& & [||rcvs(lnk(kind(e));time(e))||-||snds(lnk(kind(e));t)||]
 (& & =
 (& & msg(a(loc(e);time(e)))
 (& &  Msg) 

latex

Definitions

x:AB(x), P & Q, A & B, {i..j}, a<b, Void, x:AB(x), Msg, s = t, x:A. B(x), P  Q, False, A, AB, x:A. B(x), FairFifo, World, t  T, E, isrcv(k), time(e), loc(e), a(i;t), kind(e), lnk(k), isrcv(l;a), b, act(e), {x:A| B(x) }, , , , b, Prop, P  Q, Unit, left+right, a = b, p  q, True, T, SqStable(P), kind(a), isnull(a), P  Q, snds(l;t), ||as||, rcvs(l;t), x:A. B(x), S  T, Action(i), ij, queue(l;t), Top, type List, #$n, Type, ij, n-m, i<j, hd(l), msg(a), {T}, SQType(T), s ~ t, match(l;t;t'), IdLnk, l[i], i  j < k, concat(ll), upto(n), m(l;t), x.A(x), map(f;as), <a,b>, true, w.M, mlnk(m), -n, n+m, source(l), Id, onlnk(l;mss), Msg(M), m(i;t)

Lemmas

assert of band, and functionality wrt iff, select upto, map select, w-m wf, Msg wf, w-onlnk wf, Id wf, lsrc wf, mlnk wf, w-M wf, firstn map, firstn upto, bnot of le int, length upto, map length, select concat, concat wf, map wf, w-ml wf, int seg wf, upto wf, select wf, IdLnk wf, w-msg wf, nth tl decomp, general length nth tl, assert of lt int, squash wf, true wf, bnot of lt int, assert of le int, lt int wf, le wf, le int wf, ge wf, non neg length, length wf1, w-action wf, w-rcvs wf, nat wf, w-snds wf, w-Msg wf, top wf, w-loc wf, w-time wf, assert-eq-lnk, sq stable from decidable, decidable assert, band wf, eq lnk wf, lnk wf, w-isnull wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bnot wf, not wf, w-kind wf, w-a wf, bool wf, assert wf, isrcv wf, w-ekind wf, fair-fifo wf, w-E wf, world wf